Since 2000, the algorithmic performance of single-node sequential solvers for the Boolean Satisfiability (SAT) problem has improved by more than 1000×. While the SAT problem generally has worst-case NP-complete complexity, many structured problems do not exhibit such worst case complexity and modern solvers have evolved into highly successful tools for solving a range of practical problems including resource allocation, planning, and hardware and software verification. As a practical tool, SAT solvers fill a niche in that they can efficiently reason within a single framework about complex logical constraints that capture concepts such as coordination, deconfliction and mutual exclusion and fixed-point arithmetic constraints that can include non-linear expressions. As a practical tool, open off-the-shelf SAT solvers suffer from two key limitations.
First, each SAT problem instance input is inherently limited to a static SAT-or-UNSAT decision problem. A generic modern SAT solver, given a logical formula over a set of Boolean variables (typically a conjunction of constraints), will either return a result of SAT along with a single example assignment to the variables or else a result of UNSAT representing that the problem is unsolvable. If a second example SAT assignment is required or if the logical expression is modified, the solver must be restarted from the beginning with no retained information. While specialized solvers exist that can count the number of satisfying assignments or that provide a limited (addition of refinement constraints only) incremental solving capability, these solvers do not fully address this limitation in a practical sense and are not typically at the leading edge of performance.
Second, solvers at the leading edge of performance are aggressively optimized and notoriously difficult to either parallelize or extend. Many modern solvers accept logical expressions in Conjunctive Normal Form (CNF) and use custom data structures to access and manage clauses (disjunctions of literals) affected by a variable assignment. In addition, one of the key optimizations in modern SAT solving is to use a system for generating new learnt clauses that capture ground truths about the problem instance and concisely prune the search tree of possibly valid assignments. Although the propagation of logical implications, called Boolean Constraint Propagation (BCP), from test assignments can be parallelized in theory, the data structures and learning required to achieve top performance result in extreme non-locality of memory references and difficult synchronization requirements that have frustrated many attempts at effective fine-grained parallelism. Further, aggressive optimization tends to make the implementation fragile to modification or the addition of state to support extended features.
Some techniques describe management of an ensemble of solvers in which the solvers may communicate with each other in a peer-to-peer manner. Changes to the original problem to be solved may be communicated to the different solvers of the ensemble to facilitate incremental solving. In these techniques, however, the individual solvers typically cannot retrieve previously learned information that may still be valid after a modification of the problem and, as such, may need to regenerate such information or may need to solve the modified problem without such information. While the information about the solution to the problem may be shared, the solvers typically do not and cannot manage sharing of the information because, in general, no solver has a complete view of all of the information shared across the entire ensemble, whether previously shared information is valid after a change to the original problem.